Nuprl Lemma : assert_of_rng_eq
13,42
postcript
pdf
r
:Rng,
a
,
b
:|
r
|. (
(
a
=
b
))
(
a
=
b
)
latex
Up
rings
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
IsEqFun(
T
;
eq
)
Lemmas
rng
wf
,
rng
all
properties
origin
r:Rng, a, b:|r|. (
(a =
b)) 
(a = b) r:Rng, a, b:|r|. ((a = b)) (a = b) 
Tx:A. B(x)